A, B:Realizer.
R-interface(A;B)

(i:Id.
(R-has-loc(A;i)
( kdom(R-da(A;i)). 

( T=R-da(A;i)(k)  
( Tisrcv(k)  source(lnk(k)) = i  Id  T  R-da(B;destination(lnk(k)))(k)?Top) 

latex

Definitions

R-interface(A;B), xdom(f). v=f(x)   P(x;v), P  Q, P & Q, P  Q, Prop, Void, rcv(l,tg), IdLnk, R-has-loc(R;i), x  dom(f), b, isrcv(k), s = t, Id, source(l), f(x), f(x)?z, destination(l), lnk(k), P  Q, KindDeq, x:AB(x), R-da(R;i), x.A(x), Type, a:A fp B(a), x:A. B(x), x. t(x), Top, Knd, t  T, Realizer, tag(k), Atom$n, left+right, s ~ t, SQType(T), {T}, Unit, x:AB(x), , b, A, False, Case b of inl(x)  s(x) ; inr(y)  t(y), f(a), if b t else f fi, rec(x.A(x)), EqDecider(T), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), True, isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), Dec(P), P  Q

Lemmas

not-R-has-loc-R-da, decidable assert, deq wf, subtype rel self, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, Knd sq, isrcv-implies, Id sq, tagof wf, es realizer wf, Knd wf, top wf, fpf wf, R-da wf, fpf-trivial-subtype-top, Kind-deq wf, lnk wf, ldst wf, fpf-cap wf, fpf-ap wf, lsrc wf, Id wf, isrcv wf, assert wf, fpf-dom wf, R-has-loc wf, IdLnk wf, rcv wf